@article{pelanekSnS,
	author	= "Gerd Behrmann and Kim G. Larsen and Radek Pelánek",
	title		= "To {S}tore or {N}ot {T}o {S}tore",
	year		= "2003",
    journal     = "Computer Aided Verification (CAV 2003)"
}

@book{modelChecking,
	author	= "Edmund M. Clarke, Jr. and Orna Grumberg and Doron A. Peled",
	title		= "Model Checking",
	publisher	= "The MIT press",
	year		= "1999",
	ISBN		= "ISBN 0-262-03270-8"
}

@conference{IBMmch,
	author	= "Cindy Eisner",
	title		= "Model {C}hecking the {G}arbage {C}ollection {M}echanism of {SMV}",
	booktitle	= "CAV'01",
	year		= "2001",
}
@article{fvInSysDesign,
	author	= "Y. Abarbanel-Vinov and N. Aizenbud-Reshef and I. Beer and C. Eisner and D. Geist and T. Heyman and I. Reuveni and E. Rippel and I. Shitsevalov and Y. Wolfsthal and T. Yatzkar-Haham",
	title		= "On the effective deployment of functional formal verification",
	year		= "2001",
	journal	= "Formal Methods in System Design",
	volume	= "19"
}

@conference{mchIBMGigahertzProcessor,
	author	= "J. Baumgartner and T. Heyman and V. Singhal and A. Aziz",
	title		= "Model checking the {IBM} {G}igahertz {P}rocessor: {A}n abstraction algorithm for high-performance netlists",
	booktitle	= "11$^{th}$ International Conference on Computer Aided Verification (CAV)",
	year		= "1999",
	pages		= "72--83",
	publisher	= "Springer-Verlag"
}

@techreport{mchMicrosoft,
	author	= "Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani",
	title		= "{SLAM} and {S}tatic {D}river {V}erifier: {T}echnology {T}ransfer of {F}ormal {M}ethods inside {M}icrosoft",
	institution = "Microsoft Corporation",
	type		= "{T}echnical {R}eport",
	number	= "MSR-TR-2004-08",
	year		= "2004",
	month		= "January"
}

@conference{HWFDesignMethodology,
	author	= "C. Eisner and R. Hoover and W. Nation and K. Nelson and I. Shitsevalov and K. Valk",
	title		= "A methodology for formal design of hardware control with application to cache coherence protocols",
	booktitle	= "37$^{th}$ {D}esign {A}utomation {C}onference ({DAC})",
	pages		= "724--729",
	year		= "2000",
	month		= "June",
	publisher	= "Association for {C}omputing {M}achinery, Inc."
}

@conference{IBMfvCoreconnect,
	author	= "A.Goel and W. Lee",
	title		= "Formal verification of an {IBM} {C}oreconnect {P}rocessor {L}ocal {B}us arbiter core",
	booktitle	= "37$^{th}$ {D}esign {A}utomation {C}onference ({DAC})",
	pages		= "196--200",
	year		= "2000",
	month		= "June",
	publisher	= "Association for {C}omputing {M}achinery, Inc."
}

@article{Ball:2011:DSM:1965724.1965743,
	author	= "Ball, Thomas and Levin, Vladimir and Rajamani, Sriram K.",
	title		= "A decade of software model checking with {SLAM}",
	journal	= "Commun. ACM",
	issue_date	= "July 2011",
	volume	= "54",
	number	= "7",
	month		= jul,
	year		= "2011",
	issn		= "0001-0782",
	pages		= "68--76",
	numpages	= "9",
	acmid		= "1965743",
	publisher	= "ACM",
	address	= "New York, NY, USA",
}

@conference{slamTwoLowFalseAlarm,
	author	= "Thomas Ball and Ella Bounimova and Rahul Kumar and Vladimir Levin",
	title		= "{SLAM}2: {S}tatic {D}river {V}erification with {U}nder 4\% {F}alse {A}larms",
	booktitle	= "Formal {M}ethods in {C}omputer {A}ided {D}esign",
	year		= "2010",
	url		= "http://research.microsoft.com/en-us/projects/slam/slam2_fmcad2010_final.pdf"
}

@misc{website:SPIN,
	author	= "Bell Labs",
	title		= "Spin -- {F}ormal {V}erification",
	month		= "May",
	year		= "2013",
	url		= "http://spinroot.com/spin/whatispin.html",
    note    = "[Online; accessed 19-May-2013]"
}

@misc{website:MS:SDV,
	author	= "Microsoft",
	title		= "About Static Driver Verifier",
	month		= "May",
	year		= "2013",
	url		= "http://msdn.microsoft.com/en-us/library/windows/hardware/gg487498.aspx",
    note    = "[Online; accessed 19-May-2013]"
}

@misc{wiki:mct,
    author  = "Wikipedia",
    title   = "List of model checking tools --- Wikipedia{,} The Free Encyclopedia",
    year    = "2013",
    url     = "http://en.wikipedia.org/w/index.php?title=List_of_model_checking_tools&oldid=554949058",
    note    = "[Online; accessed 22-May-2013]"
}

@misc{website:ParaDiSe,
    author  = "Faculty of {I}nformatics{,} {M}asaryk {U}niversity",
    title   = "ParaDiSe",
    year    = "2013",
    url     = "http://paradise.fi.muni.cz/",
    note    = "[Online; accessed 19-May-2013]"
}

@misc{website:DiVinE,
    author  = "Faculty of {I}nformatics, {M}asaryk {U}niversity",
    title   = "DIVINE",
    year    = "2013",
    url     = "http://divine.fi.muni.cz/",
    note    = "[Online; accessed 19-May-2013]"
}

@incollection{art:ClusterLTLmc,
    title   = {Cluster-Based LTL Model Checking of Large Systems},
    booktitle = {Formal Methods for Components and Objects},
    year    = {2006},
    isbn    = {978-3-540-36749-9},
    volume  = {4111},
    series  = {Lecture Notes in Computer Science},
    editor  = {Boer, FrankS. and Bonsangue, MarcelloM. and Graf, Susanne and Roever, Willem-Paul},
    publisher = {Springer Berlin Heidelberg},
    author  = {Barnat, Jiří and Brim, Luboš and Černá, Ivana},
    pages   = {259-279}
}

@inproceedings{DiVinE,
    author  = {Barnat, Jiří and Brim, Luboš and Černá, Ivana and Šimeček, Pavel},
    address = {Lisboa, Portugal},
    booktitle = {In proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05)},
    keywords= {distributed; parallel; model-checking},
    language= {eng},
    location= {Lisboa, Portugal},
    pages   = {89-94},
    publisher = {TU Munchen},
    title   = {DiVinE - The Distributed Verification Environment},
    year    = {2005}
}

@INPROCEEDINGS{Hammer06tostore,
    author = {Moritz Hammer and Michael Weber},
    title = {To Store or Not To Store” reloaded: Reclaiming memory on demand},
    booktitle = {Formal Methods: Application and Technology (FMICS’2006). LNCS},
    year = {2006},
    pages = {51--66},
    publisher = {Springer}
}

@inproceedings{conf:cav:storeNoStorePelanek,
  author    = {Gerd Behrmann and Kim Guldstrand Larsen and Radek Pelánek},
  title     = {To Store or Not to Store},
  booktitle = {CAV},
  year      = {2003},
  pages     = {433-445}
}

@Book{baier2008principles,
 author = {Baier, Christel},
 title = {Principles of model checking},
 publisher = {MIT Press},
 year = {2008},
 address = {Cambridge, Mass},
 isbn = {9780262026499}
 }

@incollection{Thomas:AutomataInfObj,
 author = {Thomas, Wolfgang},
 chapter = {Automata on infinite objects},
 title = {Handbook of theoretical computer science (vol. B)},
 editor = {van Leeuwen, Jan},
 year = {1990},
 isbn = {0-444-88074-7},
 pages = {133--191},
 numpages = {59},
 acmid = {114895},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
}

@misc{wiki:LTLtoBA,
   author = "Wikipedia",
   title = "Linear temporal logic to Büchi automaton --- Wikipedia{,} The Free Encyclopedia",
   year = "2013",
   url = "http://en.wikipedia.org/w/index.php?title=Linear_temporal_logic_to_B%C3%BCchi_automaton&oldid=533165879",
   note = "[Online; accessed 22-May-2013]"
 }

@Book{hopcroft2001introduction,
 author = {Hopcroft, John},
 title = {Introduction to automata theory, languages, and computation},
 publisher = {Addison-Wesley},
 year = {2001},
 address = {Boston},
 isbn = {0201441241}
 }

@incollection{stateExplosionProblem,
author={Valmari, Antti},
title={The state explosion problem},
year={1998},
isbn={978-3-540-65306-6},
booktitle={Lectures on Petri Nets I: Basic Models},
volume={1491},
series={Lecture Notes in Computer Science},
editor={Reisig, Wolfgang and Rozenberg, Grzegorz},
publisher={Springer Berlin Heidelberg},
pages={429-528}
}
